Step of Proof: comp_id_l
12,41
postcript
pdf
Inference at
*
1
1
I
of proof for Lemma
comp
id
l
:
1.
A
: Type
2.
B
: Type
3.
f
:
A
B
(
x
.(
x
.
x
)(
f
(
x
))) =
f
latex
by Reduce 0
latex
1
:
1:
(
x
.
f
(
x
)) =
f
.
origin
B
(
x.(x.x)(f(x))) = f
by Reduce 0
1:
1: (x.f(x)) = f
.B
(x.(x.x)(f(x))) = f
by Reduce 0
1:
1: (x.f(x)) = f
.